A:Type, eq:EqDecider(A), f, g:x:A fp Top.
fpf-is-empty(f  g) ~ (fpf-is-empty(f)  fpf-is-empty(g)) 

latex

Definitions

x  dom(f), fpf-is-empty(f), f  g, a:A fp B(a), t  T, x:A. B(x), EqDecider(T), Top, x. t(x), , {T}, P  Q, SQType(T), p  q, i=j, ||as||, xL. P(x), true, (x  l), True, b, false, ij, False, A, Prop, P & Q, P  Q, Unit, as @ bs, P  Q, T, deq-member(eq;x;L), eqof(d), p  q, b, filter(P;l)

Lemmas

squash wf, true wf, add functionality wrt eq, length append, bool wf, append wf, bor wf, eqtt to assert, filter functionality, bnot thru bor, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, not wf, assert wf, non neg length, filter wf, band wf, eqof wf, bnot wf, deq-member wf, bfalse wf, l member wf, filter trivial, btrue wf, eq int wf, length wf1, bool sq, fpf wf, top wf, deq wf